es:ES, i:Id, P:(state@iProp). @i stable state.P(state)    Prop 

latex

Definitions	@i stable state.P(state)  , e@i. P(e), x. t(x), P  Q, E, loc(e), Prop, (state when e), state after e, x(s), state@i, x:A. B(x), Id, ES, T, True, t  T
Lemmas	event system wf, Id wf, true wf, squash wf, es-state wf, es-state-after wf, es-state-when wf, es-loc wf, es-E wf, alle-at wf